CSE 311: Homework 2 Part 1

Due: Thursday, April 16th by 6:00 PM

Instructions

Complete the problems on the following pages.

Collaboration policy. You are required to submit your own solutions. You are allowed to discuss the homework with other students. However, you must complete the problems in Cozy on your own. Moreover, you must be able to explain your solution at any time. We reserve ourselves the right to ask you to explain your work at any time in the course of this class.

Late policy. You have a total of three late days during the quarter, but you can only use one late day on any one homework, giving an additional day on both parts. Please plan ahead.

Solutions submission. Submit your solution at http://cozy.cs.washington.edu

• Each part of each task is listed as its own problem.

• You have unlimited attempts on each part.

• All completed parts get full credit and uncompleted parts get no credit.

• Make sure that you understand each step that Cozy performs for you. In Part 2, you will not have Cozy’s help to make sure each step is performed correctly.

Task 1 – Cozy Propositions

For each of the following, write a formal inference proof in Cozy that the claim holds.

The allowed rules for part (a) are Modus Ponens, Intro $\vee$, Elim $\vee$, Intro $\wedge$, and Elim $\wedge$. Parts (b) and (c) additionally allow Direct Proof. No other rules are permitted.

1. Given $p \wedge q \wedge r$, $s$, and $(r \wedge s) \to (u \wedge v)$, it follows that $v \wedge p$ holds.

2. Given $(s \wedge \neg q) \to (r \vee t)$, $\neg q \to (s \wedge \neg r)$, and $q \vee \neg p$, it follows that $\neg q \to (t \wedge \neg p)$ holds.

3. Given $(\neg p \vee q) \to (r \wedge s)$, $(q \vee p) \to u$, and $p$, it follows that $(p \to q) \to (r \wedge u)$ holds.

Cozy’s documentation for inference proof problems is available here.

Task 2 – Cozy Predicates

For each of the following, write a formal inference proof in Cozy that the claim holds.

In addition to Modus Ponens, Intro $\wedge$, Elim $\wedge$, and Direct Proof, your proofs are allowed to use Intro $\forall$, Elim $\forall$, Intro $\exists$, Elim $\exists$. No other rules are permitted.

1. Let $P$ and $Q$ be unary predicates defined in some fixed domain of discourse, and let $c$ be a well-known constant in the domain. Given $P(c)$ and $\forall\,x,\,(P(x) \to Q(x))$, show that $\exists\,x,\,Q(x)$.

   Remark. Socrates is a human, all humans are mortal, ergo something is mortal.

2. Let $P$ and $Q$ be unary predicates defined in some fixed domain of discourse.

   Given $\forall\,x,\,\forall\,y,\,(P(x) \to Q(y))$, show that $(\exists\,x,\,P(x)) \to \forall\,y,\,Q(y)$.

   Remark. The equivalence of $\forall\,x,\,\forall\,y,\,(P(x) \to Q(y))$ and $(\exists\,x,\,P(x)) \to \forall\,y,\,Q(y)$ is invoked implicitly in many arguments. In this problem, you are proving one direction of the biconditional.

3. Let $R$ and $S$ be binary predicates defined in some fixed domain of discourse and $c$ be a well-known constant in the domain. Given $$\forall x,\,\forall y,\,(R(x,y) \to R(y,x))$$ and $$\forall x,\,(S(c,x) \wedge \forall y,\,(S(y,x) \to R(x,y))),$$ show that $\exists x,\,\forall y,\,R(x,y)$.

   Notice that our general strategy gives no help on the first step of this proof! Forward, we have $\forall$ facts, which we should wait to use until we know what to use them for. Backward, we have an $\exists$, where we need to wait until we know what the object is that exists.

   Hint. Think about the $\exists$ first. What object do you think might satisfy this property? (There aren’t many choices!)

Cozy’s documentation for inference proof problems is available here.